Search for: All records

Although they differ in the functionality they offer, low-level systems exhibit certain patterns of design and utilization of computing resources. In this paper we examine how modalities have emerged as a common structure in formal verification of low-level software, and explain how many recent examples naturally share common structure in the relationship between the modalities and software features they are used to reason about. We explain how the concept of a resource context (a class of system resources to reason about) naturally corresponds to families of modal operators indexed by system data, and how this naturally leads to using modal assertions to describe resource elements (data in the relevant context). 

Virtual memory management (VMM) code is a critical piece of general-purpose OS kernels, but verification of this functionality is challenging due to the complexity of the hardware interface (the page tables are updated via writes to those memory locations, using addresses which are themselves virtualized). Prior work on verification of VMM code has either only handled a single address space, or trusted significant pieces of assembly code. In this paper, we introduce a modal abstraction to describe the truth of assertions relative to a specific virtual address space: [r]P indicating that P holds in the virtual address space rooted at r. Such modal assertions allow different address spaces to refer to each other, enabling complete verification of instruction sequences manipulating multiple address spaces. Using them effectively requires working with other assertions, such as points-to assertions about memory contents — which implicitly depend on the address space they are used in. We therefore define virtual points-to assertions to definitionally mimic hardware address translation, relative to a page table root. We demonstrate our approach with challenging fragments of VMM code showing that our approach handles examples beyond what prior work can address, including reasoning about a sequence of instructions as it changes address spaces. Our results are formalized for a RISC-like fragment of x86-64 assembly in Rocq.